FDL - Nuprl Definition : f2f+-p+

Nuprl Definition : f2f+-p+

11,40

f2f+-p+ ==

e',e. f2f+-pred(e',e)^+

clarification:

f2f+-p+{i:l}
f2f+-p+(es; ff; f2f+; sndr; rcvr)
== rel_plus(es-E(es); (

e',e. f2f+-pred{i:l}(es; ff; f2f+; sndr; rcvr; e'; e)))

Definitions R^+, E, x.A(x), f2f+-pred(e',e)

FDL editor aliases f2f+-p+

Definitions	R^+, E, x.A(x), f2f+-pred(e',e)
FDL editor aliases	f2f+-p+